i:Id, ds:x:Id fp Type, da:k:Knd fp Type, snd:msg-spec(ds;da).
msg-spec-loc-decl(snd;i;da)  Prop 

latex

Definitions	Void, Type, t  T, x:A. B(x), rcv(l,tg), KindDeq, Knd, x.A(x), x. t(x), f(x)?z, type List, Valtype(da;k), x:AB(x), State(ds), , x:AB(x), <a,b>, Id, 1of(t), msg-item(ds;da;k;l), a:A fp B(a), IdLnk, 2of(t), Top, x  dom(f), b, Prop, IdLnkDeq, product-deq(A;B;a;b), P  Q, f(x), map(f;as), xL. P(x), source(l), s = t, P & Q, msg-spec-loc-decl(snd;i;da), msg-spec(ds;da)
Lemmas	lsrc wf, l all wf, map wf, fpf-ap wf, product-deq wf, idlnk-deq wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, msg-item wf, pi2 wf, IdLnk wf, fpf wf, pi1 wf, Id wf, nat wf, decl-state wf, ma-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, rcv wf